STRATEGY =
(LAMBDA (X) (AND (UNIT X))) 
UNIT-PREFERENCE =NIL
MERGE =NIL
ORDER =NIL
ANCESTRY =NIL
DEPTH-BOUND =33
LENGTH-BOUND =33

PARMODULATE =NIL
ELAPSED-TIME =1700

NIL 1 2
1 ¬D(X1,B) ¬D(X1,C) AX 1
2 D(A,B) AX 3